Nuprl Lemma : comb_for_tree_leaf_wf
4,23
postcript
pdf
(
E
,
T
,
x
,
z
. tree_leaf(
x
))
E
,
T
:Type
E
True
tree_con(
E
;
T
)
latex
Definitions
T
,
x
:
A
.
B
(
x
)
,
t
T
,
True
Lemmas
true
wf
,
squash
wf
,
tree
leaf
wf
origin
E,T,x,z. tree_leaf(x)) 
E,T:Type
E
Truetree_con(E;T) E,T,x,z. tree_leaf(x)) E,T:TypeETruetree_con(E;T) T
x:A. B(x) T